Example 25 in [ Lucas - IC'06]

Summary: Ex25_Luc06

• TPDB format
• OBJ format
• Positive results:
  1. CSRPO
  2. Polynomial Interpretation
  3. CSDP
  4. Ferreira and Ribeiro's transformation
  5. Giesl and Middeldorp's transformation
  6. Lucas' transformation
  7. Zantema's transformation

Ex25_Luc06 in TPDB format ( Ex25_Luc06.trs):

			
(VAR X)
(STRATEGY CONTEXTSENSITIVE 
  (f 1)
  (c)
  (g)
  (d)
  (h 1)
)
(RULES 
f(f(X)) -> c(f(g(f(X))))
c(X) -> d(X)
h(X) -> c(d(X))
)

The CS-TRS in OBJ format (file Ex25_Luc06.obj):

			
obj Ex25_Luc06 is
  sort S .
  op f : S -> S .
  op c : S -> S [strat (0)] .
  op g : S -> S [strat (0)] .
  op d : S -> S [strat (0)] .
  op h : S -> S .
  vars X : S .
  eq f(f(X)) = c(f(g(f(X)))) .
  eq c(X) = d(X) .
  eq h(X) = c(d(X)) .
endo

Positive results

1. The µ-termination of Ex25_Luc06 can be proved by using CSRPO (computed by MuTerm)
   
2. The µ-termination of Ex25_Luc06 can be proved by using a polynomial interpretation with MuTerm
   
3. The µ-termination of Ex25_Luc06 can be proved by using CSDPs (computed by MuTerm).
   
4. The µ-termination of Ex25_Luc06 can be proved by using Ferreira and Ribeiro's transformation. The TRS Ex25_Luc06_FR:

   					
   	f(f(X)) -> c(n__f(n__g(n__f(X))))
   	c(X) -> d(activate(X))
   	h(X) -> c(n__d(X))
   	f(X) -> n__f(X)
   	g(X) -> n__g(X)
   	d(X) -> n__d(X)
   	activate(n__f(X)) -> f(activate(X))
   	activate(n__g(X)) -> g(X)
   	activate(n__d(X)) -> d(X)
   	activate(X) -> X
   
   	
   	

   can be proved terminating by AProVE.
   
5. The µ-termination of Ex25_Luc06 can be proved by using Giesl and Middeldorp's transformation. The TRS Ex25_Luc06_GM:

   					 
   	a__f(f(X)) -> a__c(f(g(f(X))))
   	a__c(X) -> d(X)
   	a__h(X) -> a__c(d(X))
   	mark(f(X)) -> a__f(mark(X))
   	mark(c(X)) -> a__c(X)
   	mark(h(X)) -> a__h(mark(X))
   	mark(g(X)) -> g(X)
   	mark(d(X)) -> d(X)
   	a__f(X) -> f(X)
   	a__c(X) -> c(X)
   	a__h(X) -> h(X)
   	
   	

   can be proved terminating by AProVE .
   
6. The µ-termination of Ex25_Luc06 can be proved by using Lucas' transformation. The TRS Ex25_Luc06_L:

   					
   	f(f(X)) -> c
   	c -> d
   	h(X) -> c
   
   	
   	

   can be proved terminating by MuTerm and polynomial interpretation
   
7. The µ-termination of Ex25_Luc06 can be proved by using Zantema's transformation. The TRS Ex25_Luc06_Z:

   					
   	f(f(X)) -> c(n__f(g(n__f(X))))
   	c(X) -> d(activate(X))
   	h(X) -> c(n__d(X))
   	f(X) -> n__f(X)
   	d(X) -> n__d(X)
   	activate(n__f(X)) -> f(X)
   	activate(n__d(X)) -> d(X)
   	activate(X) -> X
   	
   	

   can be proved terminating by AProVE .